Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))

Q is empty.


QTRS
  ↳ DirectTerminationProof

Q restricted rewrite system:
The TRS R consists of the following rules:

div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))

Q is empty.

We use [23] with the following order to prove termination.

Lexicographic path order with status [19].
Quasi-Precedence:
[div2, e, i1]

Status:
e: multiset
i1: [1]
div2: [1,2]